Nuprl Lemma : weighted-sum-nil
11,40
postcript
pdf
F
:Top. weighted-sum([];
F
) ~ 0
latex
Definitions
Top
,
t
T
,
x
:
A
.
B
(
x
)
,
ws_nil{ws_nil_compseq_tag_def:ObjectId}(
F
)
Lemmas
top
wf
origin
F:Top. weighted-sum([];F) ~ 0 F:Top. weighted-sum([];F) ~ 0 
Tx:A. B(x)